Information Flow Control For Free
Information flow control (IFC) refers to a model that focuses on determining what information is permitted to be transferred between entities in a given environment. It establishes rules for data movement, which are essential for defining security requirements. IFC can ensure that sensitive data is only accessed by authorised users, preventing data leakage or unauthorised access. One goal of IFC research is to develop language-based techniques to ensure that security policies regarding to confidentiality and integrity of data hold by construction. Dynamic IFC Theorems for Free! implements this idea as a software library rather than a standalone language, by making use of free theorems.
Free theorems can be thought of universally valid statements about polymorphic functions that do not depend on the specific types involved. They can be derived from the types of these functions alone, making them powerful tools for reasoning about program behaviour and correctness.
Tasks:
- Introduce the idea of information flow control programs by writing example programs (we recommend using lio in Haskell)
- Introduce the idea of free theorems by generating a few example free theorems (A free theorem generator) and explain how free theorems are generated (For example the paper Free Theorems Simply, via Dinaturality tries to explain how to generate free theorems, but if you search for 'theorems for free' you will also find other papers)
- Explain how "Dynamic IFC Theorems for Free!" combines these two things